$\forall$${\it es}$:ES, $i$, $a$:Id, $T$:Type, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $P$:(State(${\it ds}$)$\rightarrow$$T$$\rightarrow$Prop).
\\[0ex]@$i$ Precondition for $a$(v)$P$ State(${\it ds}$) (v:$T$) $\in$ Prop